\begin{tabbing}
combine{-}ecl{-}tuples($A$; $B$; $f$; $g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$spreadn(\=$A$;\+
\\[0ex]${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ae}$.spreadn(\=$B$;\+
\\[0ex]${\it Tb}$,${\it ksb}$,${\it ib}$,${\it gb}$,${\it hb}$,${\it ab}$,${\it be}$.$<$:${\it Ta}$ $\times$ ${\it Tb}$
\\[0ex], append(${\it ksa}$; ${\it ksb}$)
\\[0ex], $<$${\it ia}$, ${\it ib}$$>$
\\[0ex], $\lambda$${\it k'}$,$s$,$v$,$x$. $<$\=if deq{-}member(Kind{-}deq; ${\it k'}$; ${\it ksa}$)\+
\\[0ex]then ${\it ga}$(${\it k'}$,$s$,$v$,$x$.1)
\\[0ex]else $x$.1
\\[0ex]fi 
\-\\[0ex], \=if band(\=deq{-}member(Kind{-}deq; ${\it k'}$; ${\it ksb}$);\+\+
\\[0ex](${\it ha}$(0,$x$.1)))
\-\\[0ex]then ${\it gb}$(${\it k'}$,$s$,$v$,$x$.2)
\\[0ex]else $x$.2
\\[0ex]fi 
\-\\[0ex]$>$
\\[0ex], $\lambda$$n$,$x$. $f$(($\lambda$$m$.${\it ha}$($m$,$x$.1)),$\lambda$$m$.${\it hb}$($m$,$x$.2),$n$)
\\[0ex], $\lambda$$n$,${\it k'}$,$s$,$v$,$x$. \=$g$\+
\\[0ex](\=if deq{-}member(\=Kind{-}deq; ${\it k'}$; ${\it ksa}$\+\+
\\[0ex])
\-\\[0ex]then ${\it aa}$($n$,${\it k'}$,$s$,$v$,$x$.1)
\\[0ex]else ff
\\[0ex]fi 
\-\\[0ex],\=if deq{-}member(\=Kind{-}deq; ${\it k'}$; ${\it ksb}$\+\+
\\[0ex])
\-\\[0ex]then band(\=(${\it ha}$(0,$x$.1));\+
\\[0ex](${\it ab}$($n$,${\it k'}$,$s$,$v$,$x$.2)))
\-\\[0ex]else ff
\\[0ex]fi )
\-\-\\[0ex], merge(${\it ae}$; ${\it be}$)$>$))
\-\-
\end{tabbing}